Step of Proof: fseg_select
11,40
postcript
pdf
Inference at
*
2
1
1
1
2
I
of proof for Lemma
fseg
select
:
1.
T
: Type
2.
l1
:
T
List
3.
l2
:
T
List
4. ||
l1
||
||
l2
||
5.
i
:
. (
i
< ||
l1
||)
(
l1
[
i
] =
l2
[((||
l2
|| - ||
l1
||)+
i
)])
6.
i
:
7.
i
< ||
l1
||
l1
[
i
] = nth_tl(||
l2
|| - ||
l1
||;
l2
)[
i
]
latex
by ((RWO "select_nth_tl" 0)
CollapseTHEN (Auto'))
latex
C
1
:
C1:
l1
[
i
] =
l2
[(
i
+(||
l2
|| - ||
l1
||))]
C
.
Definitions
nth_tl(
n
;
as
)
,
P
Q
,
P
Q
,
l
[
i
]
,
S
T
,
|
g
|
,
{
i
..
j
}
,
A
,
False
,
P
Q
,
n
-
m
,
i
j
<
k
,
P
&
Q
,
x
:
A
B
(
x
)
,
,
#$n
,
t
T
,
a
<
b
,
,
{
x
:
A
|
B
(
x
)}
,
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
A
B
,
type
List
,
Type
,
s
=
t
,
||
as
||
,
i
j
Lemmas
iff
wf
,
rev
implies
wf
,
select
nth
tl
,
select
wf
,
le
wf
origin